﻿using System;
using System.Collections.Generic;
using System.IO;
using System.Linq;
using System.Text.RegularExpressions;
using System.Windows.Documents;

namespace RWLib
{
    public class Parser
    {
        public List<Fluent> InitialFluents { get; private set; }
        public Formula InitialFormula { get; private set; }
        public List<Fluent> Fluents { get; private set; }
        public List<Action> Actions { get; private set; }
        public List<StatementBase> ActionList { get; private set; }
        public List<StatementBase> ActionFromTextList { get; private set; }
        public String ErrorMessage { get; private set; }
        public SortedDictionary<int, List<string>> ScenarioFromText { get; set; }
        public Dictionary<String, bool> QueryFromText { get; set; }

        public Parser()
        {
            Fluents = new List<Fluent>();
            Actions = new List<Action>();
            InitialFluents = new List<Fluent>();
            ActionList = new List<StatementBase>();
            ActionFromTextList = new List<StatementBase>();
            InitialFormula = new Formula();
        }

        private void resetLists()
        {
            ActionFromTextList = new List<StatementBase>();
            ScenarioFromText = new SortedDictionary<int, List<string>>();
            InitialFluents = new List<Fluent>();
            Fluents = new List<Fluent>();
            InitialFormula = new Formula();
        }

        private Formula GetFormula(String formula, String statementName)
        {
            var formulaLower = formula.ToLower();
            //w CNF zaprzeczenie moze istniec tylko przed literalem
            if (formulaLower.Contains("not(") || formula.Contains("not (") || formula.Contains("not[") || formula.Contains("not [") ||
                formulaLower.Contains(")not") || formula.Contains(") not") || formula.Contains("]not") || formula.Contains("] not"))
            {
                ErrorMessage = "Wrong syntax in parsing the CNF in " + statementName;
                return null;
            }
            var stringSeparators = new String[] { " and ", " and(", ")and" };
            String[] results = formula.Split(stringSeparators, StringSplitOptions.RemoveEmptyEntries);
            stringSeparators = new String[] { " or ", " or(", ")or " };
            var clausesList = new List<Clause>();
            foreach (var result in results)
            {
                String r = result.Replace("(", "").Replace(")", "").Replace("[", "").Replace("]", "");
                String[] subresults = r.Split(stringSeparators, StringSplitOptions.RemoveEmptyEntries);
                var fluentsList = new List<Fluent>();
                foreach (var sr in subresults)
                {
                    var fluent = sr.Split(new[] { " " }, StringSplitOptions.RemoveEmptyEntries);
                    if (fluent.Count() == 2)
                    {
                        if (fluent[0].ToLower().Equals("not"))
                        {
                            if (!Fluents.Any(f => f.Name.Equals(fluent[1])))
                            {
                                if (statementName.Equals("query"))
                                {
                                    ErrorMessage = "Fluent(s) not defined in " + statementName;
                                    return null;
                                }
                                Fluents.Add(new Fluent(fluent[1], false, true));
                            }
                            fluentsList.Add(new Fluent(fluent[1], false, true));
                        }
                        else
                        {
                            ErrorMessage = "Wrong syntax in parsing the CNF in " + statementName;
                            return null;
                        }
                    }
                    else if (fluent.Count() == 1)
                    {
                        if (!Fluents.Any(f => f.Name.Equals(fluent[0])))
                        {
                            if (statementName.Equals("query"))
                            {
                                ErrorMessage = "Fluent(s) not defined in " + statementName;
                                return null;
                            }
                            Fluents.Add(new Fluent(fluent[0], false, false));
                        }
                        fluentsList.Add(new Fluent(fluent[0], false, false));
                    }
                    else
                    {
                        ErrorMessage = "Wrong syntax in parsing the CNF in " + statementName;
                        return null;
                    }
                }
                clausesList.Add(new Clause(fluentsList));
            }
            if (!clausesList.Any())
            {
                ErrorMessage = "Wrong syntax in parsing the CNF in " + statementName;
                return null;
            }
            return new Formula(clausesList);
        }

        private List<Fluent> getFluents(String[] words, String statement)
        {
            List<Fluent> returnedFluents = new List<Fluent>();
            String[] stringSeparators = new String[] { " and ", " and(", ")and " };
            String fluentString = String.Join(" ", words);
            String[] results = fluentString.Split(stringSeparators, StringSplitOptions.RemoveEmptyEntries);

            foreach (var result in results)
            {
                stringSeparators = new String[] { " " };
                var fluents = result.Split(stringSeparators, StringSplitOptions.RemoveEmptyEntries);
                var fluent = new Fluent(fluents.Last());
                if (fluents.Count() == 2)
                    fluent.Value = false;
                else if (fluents.Count() == 1)
                    fluent.Value = true;
                else
                {
                    ErrorMessage = "Wrong syntax in parsing fluents in " + statement;
                    return null;
                }

                if (!Fluents.Any(f => f.Name.Equals(fluent.Name)))
                    Fluents.Add(fluent);
                returnedFluents.Add(fluent);
            }
            return returnedFluents;
        }

        public Tree BuildTree(SortedDictionary<int, List<string>> scenario)
        {
            Tree t = null;
            if (ScenarioFromText == null || !ScenarioFromText.Any())
                ScenarioFromText = scenario;
            try
            {
                ErrorMessage = String.Empty;
                if (Fluents == null || !Fluents.Any())
                {
                    ErrorMessage = "There are no fluents defined";
                    Console.WriteLine(ErrorMessage);
                    return null;
                }
                foreach (var item in scenario)
                    foreach (var name in item.Value)
                        if (!ActionFromTextList.Any(a => a.Name == name))
                        {
                            ErrorMessage = "There is no action named " + name;
                            Console.WriteLine(ErrorMessage);
                            return null;
                        }
                SortedDictionary<int, List<string>> scenarioCopy = new SortedDictionary<int, List<string>>(scenario);
                Scenario sc = new Scenario(scenarioCopy, Fluents);
                foreach (var fluent in Fluents)
                {
                    bool exists = false;
                    if(InitialFormula.Conditions == null)
                        InitialFormula = new Formula(new List<Clause>());
                    foreach (var clause in InitialFormula.Conditions)
                    {
                        if (clause.Conditions.Any(f => f.Name == fluent.Name))
                        {
                            exists = true;
                            break;
                        }
                    }
                    if (!exists)
                    {
                        var fluentsList = new List<Fluent>
                            {
                                new Fluent(fluent.Name),
                                new Fluent(fluent.Name, false, true)
                            };
                        InitialFormula.Conditions.Add(new Clause(fluentsList));
                    }
                    
                }
                sc._initialFormula = InitialFormula;
                ActionDomain domain = new ActionDomain();
                domain.Triggers = new List<TriggerStatement>();
                domain.Actions = new List<StatementBase>();
                foreach (var action in ActionFromTextList)
                {
                    if (action is TriggerStatement)
                        domain.Triggers.Add((TriggerStatement)action);
                    else
                        domain.Actions.Add(action);
                }
                t = Tree.build(sc, domain, true);
            }
            catch (Exception e)
            {
                throw e;
            }
            return t;
        }

        public SortedDictionary<int, List<string>> ParseScenario(String scenario)
        {
            String[] lines = Regex.Split(scenario, "\r\n|\r|\n");
            ScenarioFromText = new SortedDictionary<int, List<string>>();
            ErrorMessage = String.Empty;

            foreach (var line in lines)
            {
                var words = line.Split(new[] { " " }, StringSplitOptions.RemoveEmptyEntries);
                if (words.Count() != 3)
                {
                    ErrorMessage = "Wrong syntax in scenario";
                    return null;
                }
                if (ActionFromTextList.Any(a => a.Name.Equals(words[0])))
                {
                    if (words[1].ToLower().Equals("at"))
                    {
                        int time;
                        if (!int.TryParse(words[2], out time))
                        {
                            ErrorMessage = "Wrong syntax in scenario";
                            return null;
                        }
                        if (time < 1 || time > 20)
                        {
                            ErrorMessage = "Wrong syntax in scenario: time can be between 1 and 20 time units";
                            return null;
                        }
                        KeyValuePair<int, List<string>> element;
                        if (ScenarioFromText.Any(s => s.Key == time))
                            ScenarioFromText.FirstOrDefault(s => s.Key == time).Value.Add(words[0]);
                        else
                            ScenarioFromText.Add(time, new List<string> { words[0] });
                    }
                    else
                    {
                        ErrorMessage = "Wrong syntax in scenario";
                        return null;
                    }
                }
                else
                {
                    ErrorMessage = "Error in scenario: there is no action named " + words[0];
                    return null;
                }
            }
            return ScenarioFromText;
        }

        public Dictionary<string, bool> ParseQueries(Tree tree, String queries)
        {
            String[] lines = Regex.Split(queries, "\r\n|\r|\n");
            QueryFromText = new Dictionary<string, bool>();
            ErrorMessage = String.Empty;

            foreach (var line in lines)
            {
                var answer = ParseQuery(tree, line);
                if (!ErrorMessage.Trim().Equals(String.Empty))
                    return null;
                if (!QueryFromText.Any(q => q.Key.ToLower().Equals(line.Trim().ToLower())))
                    QueryFromText.Add(line.Trim(), answer);
            }
            return QueryFromText;
        }

        //public bool ParseCompoundText(String text)
        //{
        //    String[] lines = Regex.Split(text, "\r\n|\r|\n");
        //    return true;
        //}

        #region Do wyklikania

        private void copyFromActionBase(StatementBase baseAction, StatementBase specificAction)
        {
            if (baseAction.StartTime > 0)
                specificAction.StartTime = baseAction.StartTime;
            if (baseAction.ImpossibleCondition != null)
                specificAction.ImpossibleCondition = baseAction.ImpossibleCondition;
            if (baseAction.ImpossibleTimes != null)
                specificAction.ImpossibleTimes = baseAction.ImpossibleTimes;
            if (baseAction.TriggeredBy != null)
                specificAction.TriggeredBy = baseAction.TriggeredBy;
        }

        /// <summary>
        /// Action causes effectFormula if conditionFormula
        /// </summary>
        /// <returns></returns>
        public StatementBase GetFluentEffectAction(string actionName, string conditionFormula, string effectsFormula)
        {
            var action = new FluentEffectStatement(actionName, GetFormula(conditionFormula, "causes"), GetFormula(effectsFormula, "causes"));
            ActionList.Add(action);
            return action;
        }

        /// <summary>
        /// Action1 invokes Action2 after Time if conditionFormula
        /// TYLKO WTEDY JAK ZOSTANIE DODANA AKCJA invokee
        /// </summary>
        /// <returns></returns>
        public StatementBase GetActionEffectAction(string invokerName, StatementBase invokee, int time, string conditionFormula)
        {
            var action = new ActionEffectStatement(invokerName, GetFormula(conditionFormula, "invokes"), invokee, time);
            ActionList.Add(action);
            return action;
        }

        /// <summary>
        /// conditionFormula triggers Action
        /// TYLKO WTEDY JAK ZOSTANIE DODANA AKCJA triggeredAction
        /// </summary>
        /// <returns></returns>
        public StatementBase GetTriggerAction(StatementBase triggeredAction, string conditionFormula)
        {
            var action = new TriggerStatement("sth", GetFormula(conditionFormula, "triggers"), triggeredAction);
            triggeredAction.TriggeredBy = action;
            ActionList.Add(action);
            return action;
        }

        /// <summary>
        /// Action releases effectFluent if conditionFormula
        /// </summary>
        /// <returns></returns>
        public StatementBase GetReleaseAction(string actionName, string conditionFormula, string effectFluent)
        {
            var action = new ReleaseStatement(actionName, GetFormula(conditionFormula, "releases"), new Fluent(effectFluent, false, false));
            ActionList.Add(action);
            return action;
        }

        /// <summary>
        /// impossible Action at Time
        /// TYLKO WTEDY JAK ZOSTANIE DODANA AKCJA action
        /// </summary>
        /// <returns></returns>
        public void AddImpossibleAtTime(StatementBase action, int time)
        {
            if (action.ImpossibleTimes == null)
                action.ImpossibleTimes = new List<int>();
            action.ImpossibleTimes.Add(time);
        }

        /// <summary>
        /// impossible Action if conditionFormula
        /// TYLKO WTEDY JAK ZOSTANIE DODANA AKCJA action
        /// </summary>
        /// <returns></returns>
        public void AddImpossibleIfCondition(StatementBase action, string conditionFormula)
        {
            action.ImpossibleCondition = GetFormula(conditionFormula, "impossible");
        }
        #endregion


        #region Statements ze stringa

        public List<Action> ParseFile(String fileName)
        {
            String fileContent = File.ReadAllText(@"Input\" + fileName + ".txt"); ;
            String[] lines = Regex.Split(fileContent, "\r\n|\r|\n");
            sortLines(lines);
            resetLists();
            ErrorMessage = String.Empty;

            foreach (var line in lines)
                if (!SplitStatements(line))
                {
                    Console.WriteLine(ErrorMessage);
                    resetLists();
                    return null;
                }

            return Actions;
        }

        public List<Action> Parse(String text)
        {
            String[] lines = Regex.Split(text, "\r\n|\r|\n");
            sortLines(lines);
            resetLists();
            ErrorMessage = String.Empty;

            foreach (var line in lines)
                if (!SplitStatements(line))
                {
                    Console.WriteLine(ErrorMessage);
                    resetLists();
                    return null;
                }

            return Actions;
        }

        private string[] sortLines(String[] lines)
        {
            int i = 0;
            int j = lines.Count() - 1;

            while (i < j)
            {
                String[] words = lines[i].Split(' ');
                if (!words.Any(w => w.ToLower().Equals("triggers")) &&
                    !words.Any(w => w.ToLower().Equals("impossible")) &&
                    !words.Any(w => w.ToLower().Equals("invokes")))
                {
                    i++;
                    continue;
                }
                words = lines[j].Split(' ');
                if (!words.Any(w => w.ToLower().Equals("triggers")) &&
                    !words.Any(w => w.ToLower().Equals("impossible")) &&
                    !words.Any(w => w.ToLower().Equals("invokes")))
                {
                    var temp = lines[i];
                    lines[i] = lines[j];
                    lines[j] = temp;
                    i++;
                    j--;
                }
                else
                    j--;
            }
            return lines;
        }

        private bool SplitStatements(String line)
        {
            String[] words = line.Split(new string[] { " " }, StringSplitOptions.RemoveEmptyEntries);
            if (words.Any(w => w.ToLower().Equals("initially")))
                return handleInitially(words);
            else if (words.Any(w => w.ToLower().Equals("causes")))
                return handleCauses(words);
            else if (words.Any(w => w.ToLower().Equals("invokes")))
                return handleInvokes(words);
            else if (words.Any(w => w.ToLower().Equals("triggers")))
                return handleTriggers(words);
            else if (words.Any(w => w.ToLower().Equals("releases")))
                return handleReleases(words);
            else if (words.Any(w => w.ToLower().Equals("impossible")))
                return handleImpossible(words);
            else if (words.Any(w => w.ToLower().Equals("fluents:")))
                return handleFluents(words);
            else
            {
                ErrorMessage = "Wrong syntax";
                return false;
            }
        }

        private bool handleImpossible(String[] words)
        {
            //Action action = new Action(), tempA;
            String statementName = "impossible";
            StatementBase action;
            if (words.Count() < 4)
            {
                ErrorMessage = "Wrong syntax in " + statementName;
                return false;
            }
            if ((action = ActionFromTextList.FirstOrDefault(a => a.Name == words[1])) == null)
            {
                ErrorMessage = "Error in " + statementName + ": there is no action " + words[1] + " defined yet.";
                return false;
            }

            if (words[0].ToLower().Equals("impossible"))
            {
                if (words[2].ToLower().Equals("at") && words.Count() == 4)
                {
                    if (action.ImpossibleTimes == null)
                        action.ImpossibleTimes = new List<int>();
                    int time;
                    if (!int.TryParse(words[3], out time))
                    {
                        ErrorMessage = "Wrong syntax in " + statementName + ": time is not a number";
                        return false;
                    }
                    action.ImpossibleTimes.Add(time);
                }
                else if (words[2].ToLower().Equals("if"))
                {
                    String formula = String.Join(" ", words.Skip(3));
                    var formulaObject = GetFormula(formula, statementName);
                    if (formulaObject == null)
                        return false;
                    action.ImpossibleCondition = formulaObject;
                }
                else
                {
                    ErrorMessage = "Wrong syntax in " + statementName;
                    return false;
                }
            }
            else
            {
                ErrorMessage = "Wrong syntax in " + statementName;
                return false;
            }
            return true;
        }

        private bool handleReleases(String[] words)
        {
            StatementBase action;
            String actionName, fluentName;
            String statementName = "releases";

            if (words.Count() < 3)
            {
                ErrorMessage = "Wrong syntax in " + statementName;
                return false;
            }

            actionName = words[0];
            fluentName = words[2];

            if (words[1].ToLower().Equals(statementName))
            {
                if (words.Count() > 3 && words[3].ToLower().Equals("if"))
                {
                    String formula = String.Join(" ", words.Skip(4));
                    var formulaObject = GetFormula(formula, statementName);
                    if (formulaObject == null)
                        return false;
                    action = new ReleaseStatement(actionName, formulaObject, new Fluent(fluentName, false));
                }
                else if (words.Count() == 3)
                    action = new ReleaseStatement(actionName, new Formula(), new Fluent(fluentName, false));
                else
                {
                    ErrorMessage = "Wrong syntax in " + statementName;
                    return false;
                }
                Fluents.Add(new Fluent(fluentName));
                ActionFromTextList.Add(action);
            }
            else
            {
                ErrorMessage = "Wrong syntax in " + statementName;
                return false;
            }
            return true;
        }

        private bool handleTriggers(String[] words)
        {
            TriggerStatement statement;
            StatementBase triggeredAction;
            String statementName = "triggers";

            if (words.Count() < 3)
            {
                ErrorMessage = "Wrong syntax in " + statementName;
                return false;
            }
            if ((triggeredAction = ActionFromTextList.FirstOrDefault(a => a.Name == words.Last())) == null)
            {
                ErrorMessage = "Error in " + statementName + ": there is no action " + words.Last() + " defined yet.";
                return false;
            }

            if (words[words.Count() - 2].ToLower().Equals(statementName))
            {
                String formula = String.Join(" ", words.Take(words.Count() - 2));
                var formulaObject = GetFormula(formula, statementName);
                if (formulaObject == null)
                    return false;
                statement = new TriggerStatement(formula, formulaObject, triggeredAction);
                triggeredAction.TriggeredBy = statement;
                ActionFromTextList.Add(statement);
            }
            else
            {
                ErrorMessage = "Wrong syntax in " + statementName;
                return false;
            }
            return true;
        }

        private bool handleInvokes(String[] words)
        {
            StatementBase action;
            String actionName;
            int after;
            StatementBase actionInvoked;
            String statementName = "invokes";

            if (words.Count() < 5)
            {
                ErrorMessage = "Wrong syntax in " + statementName;
                return false;
            }
            if ((actionInvoked = ActionFromTextList.FirstOrDefault(a => a.Name == words[2])) == null)
            {
                ErrorMessage = "Error in " + statementName + ": there is no action " + words[2] + " defined yet.";
                return false;
            }
            actionName = words[0];

            if (!(words[1].ToLower().Equals(statementName) && words[3].ToLower().Equals("after")))
            {
                ErrorMessage = "Wrong syntax in " + statementName;
                return false;
            }
            if (!int.TryParse(words[4], out after))
            {
                ErrorMessage = "Wrong syntax in " + statementName + ": time is not a number";
                return false;
            }

            if (words.Count() > 5)
            {
                if (!words[5].ToLower().Equals("if"))
                {
                    ErrorMessage = "Wrong syntax in " + statementName;
                    return false;
                }
                String formula = String.Join(" ", words.Skip(6));
                var formulaObject = GetFormula(formula, statementName);
                if (formulaObject == null)
                    return false;
                action = new ActionEffectStatement(actionName, formulaObject, actionInvoked, after);
            }
            else
                action = new ActionEffectStatement(actionName, new Formula(), actionInvoked, after);
            ActionFromTextList.Add(action);
            return true;
        }

        private bool handleCauses(String[] words)
        {
            StatementBase action;
            String actionName;
            String statementName = "causes";

            if (words.Count() < 3)
            {
                ErrorMessage = "Wrong syntax in " + statementName;
                return false;
            }
            actionName = words[0];

            if (words[1].ToLower().Equals(statementName))
            {
                String[] stringSeparators = new String[] { " if ", ")if ", " if(" };
                String formulas = String.Join(" ", words.Skip(2));
                String[] results = formulas.Split(stringSeparators, StringSplitOptions.RemoveEmptyEntries);

                if (results.Count() == 2)
                {
                    var conditionFormulaObject = GetFormula(results[1], statementName);
                    var effectsFormulaObject = GetFormula(results[0], statementName);
                    if (conditionFormulaObject == null || effectsFormulaObject == null)
                        return false;
                    action = new FluentEffectStatement(actionName, conditionFormulaObject, effectsFormulaObject);
                }
                else if (results.Count() == 1)
                {
                    var effectsFormulaObject = GetFormula(results[0], statementName);
                    if (effectsFormulaObject == null)
                        return false;
                    action = new FluentEffectStatement(actionName, new Formula(), effectsFormulaObject);
                }
                else
                {
                    ErrorMessage = "Wrong syntax in " + statementName;
                    return false;
                }
            }
            else
            {
                ErrorMessage = "Wrong syntax in " + statementName;
                return false;
            }
            ActionFromTextList.Add(action);
            return true;
        }

        private bool handleInitially(String[] words)
        {
            String statementName = "initially";

            if (words[0].ToLower().Equals(statementName))
            {
                if (words.Count() != 1)
                {
                    var formulaObject = GetFormula(String.Join(" ", words.Skip(1)), statementName);
                    if (formulaObject == null)
                        return false;
                    InitialFormula = formulaObject;
                }
                //var fluentsObjects = getFluents((words.Skip(1).ToArray()), statementName);
                //if (fluentsObjects == null)
                //    return false;
                //var fluents = fluentsObjects.Copy();
                //InitialFluents.AddRange(fluents);
            }
            else
            {
                ErrorMessage = "Wrong syntax in " + statementName;
                return false;
            }
            return true;
        }

        private bool handleFluents(String[] words)
        {
            String statementName = "fluents";

            if (words[0].ToLower().Contains(String.Concat(statementName, ":")))
            {
                var fluents = String.Join(" ", words).Split(new[] { ":", "," }, StringSplitOptions.RemoveEmptyEntries);
                fluents = fluents.Skip(1).ToArray();
                foreach (var f in fluents)
                {
                    var fluent = f.Trim().Split(new[] { " " }, StringSplitOptions.RemoveEmptyEntries);
                    if (fluent.Count() != 1)
                    {
                        ErrorMessage = "Wrong syntax in parsing the list of fluents";
                        return false;
                    }
                    Fluents.Add(new Fluent(f.Trim()));
                }
            }
            else
            {
                ErrorMessage = "Wrong syntax in " + statementName;
                return false;
            }
            return true;
        }

        #endregion


        #region Queries


        public bool ParseQuery(Tree tree, String query)
        {
            String[] words = query.Split(new string[] { " " }, StringSplitOptions.RemoveEmptyEntries);
            ErrorMessage = String.Empty;
            bool answer = false;

            if (words.Any(w => w.ToLower().Equals("always")))
            {
                if (words.Any(w => w.ToLower().Equals("executable")))
                    answer = alwaysExecutableParse(tree, words);
                else if (words.Any(w => w.ToLower().Equals("true")))
                    answer = alwaysTrueParse(tree, words);
                else if (words.Any(w => w.ToLower().Equals("reachable")))
                    answer = alwaysReachableParse(tree, words);
                else
                    ErrorMessage = "Wrong syntax in query";
            }
            else if (words.Any(w => w.ToLower().Equals("sometimes")))
            {
                if (words.Any(w => w.ToLower().Equals("executable")))
                    answer = sometimesExecutableParse(tree, words);
                else if (words.Any(w => w.ToLower().Equals("true")))
                    answer = sometimesTrueParse(tree, words);
                else if (words.Any(w => w.ToLower().Equals("reachable")))
                    answer = sometimesReachableParse(tree, words);
                else
                    ErrorMessage = "Wrong syntax in query";
            }
            else if (words.Any(w => w.ToLower().Equals("executable")))
            {
                answer = actionExecutableParse(tree, words);
            }
            else
            {
                ErrorMessage = "Wrong syntax in query";
            }

            if (ErrorMessage.Length > 0)
            {
                Console.WriteLine(ErrorMessage);
                return false;
            }

            return answer;
        }

        /// <summary>
        /// Scenario executability query: always executable Sc
        /// </summary>
        /// <param name="query"></param>
        /// <returns></returns>
        private bool alwaysExecutableParse(Tree tree, String[] words)
        {
            if (String.Join(" ", words).ToLower().Equals("always executable sc"))
                return (new AlwaysExecutableQuery(tree, new Scenario(ScenarioFromText, Fluents))).Run();
            ErrorMessage = "Wrong syntax in query";
            return false;
        }

        /// <summary>
        /// Scenario executability query: sometimes executable Sc
        /// </summary>
        /// <param name="query"></param>
        /// <returns></returns>
        private bool sometimesExecutableParse(Tree tree, String[] words)
        {
            if (String.Join(" ", words).ToLower().Equals("sometimes executable sc"))
                return (new SometimesExecutableQuery(tree, new Scenario(ScenarioFromText, Fluents))).Run();
            ErrorMessage = "Wrong syntax in query";
            return false;
        }

        /// <summary>
        /// Condition query: gamma always true at Time during Sc
        /// </summary>
        /// <param name="query"></param>
        /// <returns></returns>
        private bool alwaysTrueParse(Tree tree, String[] words)
        {
            var length = words.Count();
            if (words.Count() >= 7 && words.Last().ToLower().Equals("sc") && words[length - 2].ToLower().Equals("during"))
            {

                if (words[length - 4].ToLower().Equals("at") && words[length - 5].ToLower().Equals("true") &&
                    words[length - 6].ToLower().Equals("always"))
                {
                    int time;
                    if (!int.TryParse(words[length - 3], out time))
                    {
                        ErrorMessage = "Error in query: time is not a number";
                        return false;
                    }
                    var formula = String.Join(" ", words.Take(length - 6));
                    var formulaObject = GetFormula(formula, "query");
                    if (formulaObject == null)
                        return false;
                    return (new AlwaysConditionQuery(tree, formulaObject, time)).Run();
                }
                else
                    ErrorMessage = "Wrong syntax in query";
            }
            else
                ErrorMessage = "Wrong syntax in query";
            return false;
        }

        /// <summary>
        /// Condition query: gamma sometimes true at Time during Sc
        /// </summary>
        /// <param name="query"></param>
        /// <returns></returns>
        private bool sometimesTrueParse(Tree tree, String[] words)
        {
            var length = words.Count();
            if (words.Count() >= 7 && words.Last().ToLower().Equals("sc") && words[length - 2].ToLower().Equals("during"))
            {

                if (words[length - 4].ToLower().Equals("at") && words[length - 5].ToLower().Equals("true") &&
                    words[length - 6].ToLower().Equals("sometimes"))
                {
                    int time;
                    if (!int.TryParse(words[length - 3], out time))
                    {
                        ErrorMessage = "Error in query: time is not a number";
                        return false;
                    }
                    var formula = String.Join(" ", words.Take(length - 6));
                    var formulaObject = GetFormula(formula, "query");
                    if (formulaObject == null)
                        return false;
                    return (new SometimesConditionQuery(tree, formulaObject, time)).Run();
                }
                else
                    ErrorMessage = "Wrong syntax in query";
            }
            else
                ErrorMessage = "Wrong syntax in query";
            return false;
        }

        /// <summary>
        /// Goal query: gamma always reachable after Sc
        /// </summary>
        /// <param name="query"></param>
        /// <returns></returns>
        private bool alwaysReachableParse(Tree tree, String[] words)
        {
            var length = words.Count();
            if (words.Count() >= 5 && words.Last().ToLower().Equals("sc") && words[length - 2].ToLower().Equals("after") &&
                words[length - 3].ToLower().Equals("reachable") && words[length - 4].ToLower().Equals("always"))
            {
                var formula = String.Join(" ", words.Take(length - 4));
                var formulaObject = GetFormula(formula, "query");
                if (formulaObject == null)
                    return false;
                return (new AlwaysReachableQuery(tree, formulaObject)).Run();
            }
            else
                ErrorMessage = "Wrong syntax in query";
            return false;
        }

        /// <summary>
        /// Goal query: gamma sometimes reachable after Sc
        /// </summary>
        /// <param name="query"></param>
        /// <returns></returns>
        private bool sometimesReachableParse(Tree tree, String[] words)
        {
            var length = words.Count();
            if (words.Count() >= 5 && words.Last().ToLower().Equals("sc") && words[length - 2].ToLower().Equals("after") &&
                words[length - 3].ToLower().Equals("reachable") && words[length - 4].ToLower().Equals("sometimes"))
            {
                var formula = String.Join(" ", words.Take(length - 4));
                var formulaObject = GetFormula(formula, "query");
                if (formulaObject == null)
                    return false;
                return (new SometimesReachableQuery(tree, formulaObject)).Run();
            }
            else
                ErrorMessage = "Wrong syntax in query";
            return false;
        }

        /// <summary>
        /// Action executability query: a executable during Sc
        /// </summary>
        /// <param name="query"></param>
        /// <returns></returns>
        private bool actionExecutableParse(Tree tree, String[] words)
        {
            if (words.Count() == 4 && words[3].ToLower().Equals("sc") && words[2].ToLower().Equals("during") &&
                words[1].ToLower().Equals("executable"))
            {
                if (!ActionFromTextList.Any(a => a.Name.Equals(words[0])))
                {
                    ErrorMessage = "Error in query: there is no action named " + words[0];
                    return false;
                }

                return (new ActionExecutabilityQuery(tree, words[0])).Run();
            }
            else
                ErrorMessage = "Wrong syntax in query";
            return false;
        }

        #endregion
    }
}
